Quantifier instantiation via simplistic E-matching #8224

tautschnig · 2024-02-27T20:56:15Z

Use E-matching on index expressions to instantiate quantifiers when eager instantiation (aka enumerative instantiation) cannot be applied.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2024-02-27T21:22:08Z

Despite this being a "draft" PR I would like to ask for feedback on the following aspects:

@remi-delmas-3000 on the overall PR and specifically on the Quantifiers-unbounded-array-overflow test case: we'll have to clean this up to make clear what assertions we really expect to fail.
@kroening and @martin-cs : the expression matching implementation is really crude. Any and all suggestions would be most appreciated.

codecov · 2024-03-05T14:15:11Z

Codecov Report

❌ Patch coverage is 80.30303% with 13 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.01%. Comparing base (945c1e0) to head (d7eba68).

Files with missing lines	Patch %	Lines
src/solvers/flattening/boolbv_quantifier.cpp	80.30%	13 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8224   +/-   ##
========================================
  Coverage    80.00%   80.01%           
========================================
  Files         1700     1700           
  Lines       188257   188318   +61     
  Branches        73       73           
========================================
+ Hits        150615   150679   +64     
+ Misses       37642    37639    -3

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

tautschnig · 2024-03-22T10:57:00Z

@remi-delmas-3000 on the overall PR and specifically on the Quantifiers-unbounded-array-overflow test case: we'll have to clean this up to make clear what assertions we really expect to fail.

This is now done, comment explaining the (expected) verification failure is now included.

kroening · 2024-05-01T16:58:40Z

This needs serious consideration: failing quantifier instantiation is the leading source of proof brittleness, and we are opening the door to that here.

kroening · 2024-05-01T16:59:06Z

I would much prefer a more deterministic, predictable and robust solution to this.

martin-cs · 2024-05-05T21:14:34Z

Hard maybe?

So, it would be good but there is going to be a limit on how much we can do like this. Unless we put a refinement loop around the solver and do something like MBQI. Getting that stable and reliable is tricky. Given the amount of work that has gone into E-matching in Z3 and Andy's decade+ of work on quantifiers in cvc5, I wonder whether it would be more efficient (in terms of dev-hours / things proved) to improve our SMT integration.

To actually answer the question you asked, things that might help:

Make sure both the terms in the quantifiers and the expressions you are using as context are rewritten.
Use a union-find so that "up to equality" is handled. The modern approach might be to use an E-Graph data structure for both this and previous.
You can do a number of optimisations if the quantified variable(s) are only used once in the body or are only used in one atom. That should handle the simple cases but when you have \forall x, y, z . p(x,y) && q(y,z) && r(x,z) I think you need to get into term indexing and ordering the matching.

HTH

conjunction(...) and disjunction(...) helper functions produce the appropriate result for empty operand sequences.

Copilot

Pull request overview

This PR implements quantifier instantiation via E-matching for cases where eager (enumerative) instantiation cannot be applied. The implementation uses pattern matching on array index expressions to find suitable instantiation values from the solver's cache.

Key changes:

Added E-matching based quantifier instantiation as a fallback when eager instantiation fails
Removed the lb > ub check in eager instantiation (correctly handles empty ranges with vacuous truth/false)
Updated test expectations to reflect that previously unsupported quantifier cases now work

Reviewed changes

Copilot reviewed 10 out of 10 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/solvers/flattening/boolbv_quantifier.cpp	Implements E-matching algorithm via `instantiate_one_quantifier` function and modifies `finish_eager_conversion_quantifiers` to apply it
regression/cbmc/Quantifiers-unbounded-array/test.desc	Test descriptor for new unbounded array quantifier test case
regression/cbmc/Quantifiers-unbounded-array/main.c	Test case demonstrating quantifier instantiation with unbounded arrays and loop invariants
regression/cbmc/Quantifiers-unbounded-array-overflow/test.desc	Test descriptor for overflow detection with quantifiers
regression/cbmc/Quantifiers-unbounded-array-overflow/main.c	Test case that validates overflow detection in loop invariants with quantifiers
regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.desc	Test descriptor for 2D array quantifier handling
regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.c	Test case for nested quantifiers over 2D arrays
regression/cbmc/Quantifiers-type/test.desc	Updated test expectations to reflect working quantifier support
regression/cbmc/Quantifiers-invalid-var-range/test.desc	Updated test expectations from KNOWNBUG to CORE status
doc/cprover-manual/cbmc-assertions.md	Updated documentation from "future releases will support" to "CPROVER supports" for quantifiers

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2025-12-19T15:13:45Z

src/solvers/flattening/boolbv_quantifier.cpp

+  else
+    return conjunction(instantiations);


Missing defensive check for quantifier type. Add an assertion or UNREACHABLE statement after the if-else chain to handle the case where q_expr.id() is neither ID_exists nor ID_forall, similar to the pattern used in eager_quantifier_instantiation at line 265.

Suggested change

else

return conjunction(instantiations);

else if(q_expr.id() == ID_forall)

return conjunction(instantiations);

UNREACHABLE;

return {};

Copilot · 2025-12-19T15:13:45Z

regression/cbmc/Quantifiers-unbounded-array-overflow/test.desc

+--
+Uses --no-standard-checks to contain verification time with MiniSat; with
+CaDiCaL this completes in under 5 seconds either way. Takes an unknown amount of
+time (has never been run to completition) when using Z3.


Spelling error in comment: "completition" should be "completion".

Suggested change

time (has never been run to completition) when using Z3.

time (has never been run to completion) when using Z3.

Copilot · 2025-12-19T15:13:45Z

src/solvers/flattening/boolbv_quantifier.cpp

 #include "boolbv.h"



Duplicate include directive detected. The header "boolbv.h" is included twice on consecutive lines. Remove one of these duplicate includes.

Suggested change

#include "boolbv.h"

Use E-matching on index expressions to instantiate quantifiers when eager instantiation (aka enumerative instantiation) cannot be applied.

tautschnig force-pushed the features/quantifiers-elimination branch from e08d98e to 24806af Compare February 27, 2024 21:23

tautschnig assigned tautschnig, kroening, remi-delmas-3000 and martin-cs Feb 27, 2024

tautschnig added the Solvers label Feb 27, 2024

tautschnig force-pushed the features/quantifiers-elimination branch from 24806af to 69f8720 Compare March 5, 2024 13:43

tautschnig removed their assignment Mar 5, 2024

tautschnig marked this pull request as ready for review March 5, 2024 14:06

tautschnig requested review from TGWDB, jimgrundy, kroening, martin-cs and peterschrammel as code owners March 5, 2024 14:06

tautschnig force-pushed the features/quantifiers-elimination branch from 6e48e44 to 49b3909 Compare March 5, 2024 15:15

tautschnig self-assigned this Mar 5, 2024

tautschnig force-pushed the features/quantifiers-elimination branch 2 times, most recently from 7bb221f to 64252a0 Compare March 6, 2024 08:59

tautschnig force-pushed the features/quantifiers-elimination branch 2 times, most recently from d821caa to 090c84a Compare March 22, 2024 10:55

tautschnig unassigned remi-delmas-3000 and tautschnig Mar 22, 2024

tautschnig force-pushed the features/quantifiers-elimination branch from 090c84a to 72550cf Compare March 22, 2024 11:12

tautschnig force-pushed the features/quantifiers-elimination branch from 72550cf to 5e379d6 Compare June 11, 2024 12:23

tautschnig mentioned this pull request Jun 11, 2024

CBMC wavefront does not terminate on simple decreases clause in loop #8301

Open

tautschnig force-pushed the features/quantifiers-elimination branch from 5e379d6 to e076dab Compare July 12, 2024 11:38

tautschnig assigned tautschnig and unassigned kroening and martin-cs Jul 12, 2024

tautschnig force-pushed the features/quantifiers-elimination branch 2 times, most recently from 2a85427 to 9be48ee Compare March 25, 2025 10:28

Eager quantifier elimination: support empty ranges

c6b125d

conjunction(...) and disjunction(...) helper functions produce the appropriate result for empty operand sequences.

Copilot AI review requested due to automatic review settings December 19, 2025 15:09

tautschnig force-pushed the features/quantifiers-elimination branch from 9be48ee to 9e896a5 Compare December 19, 2025 15:09

Copilot started reviewing on behalf of tautschnig December 19, 2025 15:09 View session

Copilot AI reviewed Dec 19, 2025

View reviewed changes

Quantifier instantiation via simplistic E-matching

d7eba68

Use E-matching on index expressions to instantiate quantifiers when eager instantiation (aka enumerative instantiation) cannot be applied.

tautschnig force-pushed the features/quantifiers-elimination branch from 9e896a5 to d7eba68 Compare December 19, 2025 15:28

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Quantifier instantiation via simplistic E-matching #8224

Quantifier instantiation via simplistic E-matching #8224

Uh oh!

tautschnig commented Feb 27, 2024 •

edited

Loading

Uh oh!

tautschnig commented Feb 27, 2024

Uh oh!

codecov bot commented Mar 5, 2024 •

edited

Loading

Uh oh!

tautschnig commented Mar 22, 2024

Uh oh!

kroening commented May 1, 2024

Uh oh!

kroening commented May 1, 2024

Uh oh!

martin-cs commented May 5, 2024

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Dec 19, 2025

Uh oh!

Copilot AI Dec 19, 2025

Uh oh!

Copilot AI Dec 19, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

-  else
-    return conjunction(instantiations);
+  else if(q_expr.id() == ID_forall)
+    return conjunction(instantiations);
+  UNREACHABLE;
+  return {};

	time (has never been run to completition) when using Z3.
	time (has never been run to completion) when using Z3.

Quantifier instantiation via simplistic E-matching #8224

Are you sure you want to change the base?

Quantifier instantiation via simplistic E-matching #8224

Uh oh!

Conversation

tautschnig commented Feb 27, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Feb 27, 2024

Uh oh!

codecov bot commented Mar 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

tautschnig commented Mar 22, 2024

Uh oh!

kroening commented May 1, 2024

Uh oh!

kroening commented May 1, 2024

Uh oh!

martin-cs commented May 5, 2024

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Dec 19, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 19, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 19, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

tautschnig commented Feb 27, 2024 •

edited

Loading

codecov bot commented Mar 5, 2024 •

edited

Loading